minus(s(x), y) → if(gt(s(x), y), x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
gcd(x, y) → if1(ge(x, y), x, y)
if1(true, x, y) → if2(gt(y, 0), x, y)
if1(false, x, y) → if3(gt(x, 0), x, y)
if2(true, x, y) → gcd(minus(x, y), y)
if2(false, x, y) → x
if3(true, x, y) → gcd(x, minus(y, x))
if3(false, x, y) → y
gt(0, y) → false
gt(s(x), 0) → true
gt(s(x), s(y)) → gt(x, y)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
↳ QTRS
↳ Overlay + Local Confluence
minus(s(x), y) → if(gt(s(x), y), x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
gcd(x, y) → if1(ge(x, y), x, y)
if1(true, x, y) → if2(gt(y, 0), x, y)
if1(false, x, y) → if3(gt(x, 0), x, y)
if2(true, x, y) → gcd(minus(x, y), y)
if2(false, x, y) → x
if3(true, x, y) → gcd(x, minus(y, x))
if3(false, x, y) → y
gt(0, y) → false
gt(s(x), 0) → true
gt(s(x), s(y)) → gt(x, y)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
minus(s(x), y) → if(gt(s(x), y), x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
gcd(x, y) → if1(ge(x, y), x, y)
if1(true, x, y) → if2(gt(y, 0), x, y)
if1(false, x, y) → if3(gt(x, 0), x, y)
if2(true, x, y) → gcd(minus(x, y), y)
if2(false, x, y) → x
if3(true, x, y) → gcd(x, minus(y, x))
if3(false, x, y) → y
gt(0, y) → false
gt(s(x), 0) → true
gt(s(x), s(y)) → gt(x, y)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
gcd(x0, x1)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
if3(true, x0, x1)
if3(false, x0, x1)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
MINUS(s(x), y) → IF(gt(s(x), y), x, y)
MINUS(s(x), y) → GT(s(x), y)
IF(true, x, y) → MINUS(x, y)
GCD(x, y) → IF1(ge(x, y), x, y)
GCD(x, y) → GE(x, y)
IF1(true, x, y) → IF2(gt(y, 0), x, y)
IF1(true, x, y) → GT(y, 0)
IF1(false, x, y) → IF3(gt(x, 0), x, y)
IF1(false, x, y) → GT(x, 0)
IF2(true, x, y) → GCD(minus(x, y), y)
IF2(true, x, y) → MINUS(x, y)
IF3(true, x, y) → GCD(x, minus(y, x))
IF3(true, x, y) → MINUS(y, x)
GT(s(x), s(y)) → GT(x, y)
GE(s(x), s(y)) → GE(x, y)
minus(s(x), y) → if(gt(s(x), y), x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
gcd(x, y) → if1(ge(x, y), x, y)
if1(true, x, y) → if2(gt(y, 0), x, y)
if1(false, x, y) → if3(gt(x, 0), x, y)
if2(true, x, y) → gcd(minus(x, y), y)
if2(false, x, y) → x
if3(true, x, y) → gcd(x, minus(y, x))
if3(false, x, y) → y
gt(0, y) → false
gt(s(x), 0) → true
gt(s(x), s(y)) → gt(x, y)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
gcd(x0, x1)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
if3(true, x0, x1)
if3(false, x0, x1)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
MINUS(s(x), y) → IF(gt(s(x), y), x, y)
MINUS(s(x), y) → GT(s(x), y)
IF(true, x, y) → MINUS(x, y)
GCD(x, y) → IF1(ge(x, y), x, y)
GCD(x, y) → GE(x, y)
IF1(true, x, y) → IF2(gt(y, 0), x, y)
IF1(true, x, y) → GT(y, 0)
IF1(false, x, y) → IF3(gt(x, 0), x, y)
IF1(false, x, y) → GT(x, 0)
IF2(true, x, y) → GCD(minus(x, y), y)
IF2(true, x, y) → MINUS(x, y)
IF3(true, x, y) → GCD(x, minus(y, x))
IF3(true, x, y) → MINUS(y, x)
GT(s(x), s(y)) → GT(x, y)
GE(s(x), s(y)) → GE(x, y)
minus(s(x), y) → if(gt(s(x), y), x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
gcd(x, y) → if1(ge(x, y), x, y)
if1(true, x, y) → if2(gt(y, 0), x, y)
if1(false, x, y) → if3(gt(x, 0), x, y)
if2(true, x, y) → gcd(minus(x, y), y)
if2(false, x, y) → x
if3(true, x, y) → gcd(x, minus(y, x))
if3(false, x, y) → y
gt(0, y) → false
gt(s(x), 0) → true
gt(s(x), s(y)) → gt(x, y)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
gcd(x0, x1)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
if3(true, x0, x1)
if3(false, x0, x1)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
↳ QDP
GE(s(x), s(y)) → GE(x, y)
minus(s(x), y) → if(gt(s(x), y), x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
gcd(x, y) → if1(ge(x, y), x, y)
if1(true, x, y) → if2(gt(y, 0), x, y)
if1(false, x, y) → if3(gt(x, 0), x, y)
if2(true, x, y) → gcd(minus(x, y), y)
if2(false, x, y) → x
if3(true, x, y) → gcd(x, minus(y, x))
if3(false, x, y) → y
gt(0, y) → false
gt(s(x), 0) → true
gt(s(x), s(y)) → gt(x, y)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
gcd(x0, x1)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
if3(true, x0, x1)
if3(false, x0, x1)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
↳ QDP
GE(s(x), s(y)) → GE(x, y)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
gcd(x0, x1)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
if3(true, x0, x1)
if3(false, x0, x1)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
gcd(x0, x1)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
if3(true, x0, x1)
if3(false, x0, x1)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
GE(s(x), s(y)) → GE(x, y)
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
GT(s(x), s(y)) → GT(x, y)
minus(s(x), y) → if(gt(s(x), y), x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
gcd(x, y) → if1(ge(x, y), x, y)
if1(true, x, y) → if2(gt(y, 0), x, y)
if1(false, x, y) → if3(gt(x, 0), x, y)
if2(true, x, y) → gcd(minus(x, y), y)
if2(false, x, y) → x
if3(true, x, y) → gcd(x, minus(y, x))
if3(false, x, y) → y
gt(0, y) → false
gt(s(x), 0) → true
gt(s(x), s(y)) → gt(x, y)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
gcd(x0, x1)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
if3(true, x0, x1)
if3(false, x0, x1)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
GT(s(x), s(y)) → GT(x, y)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
gcd(x0, x1)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
if3(true, x0, x1)
if3(false, x0, x1)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
gcd(x0, x1)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
if3(true, x0, x1)
if3(false, x0, x1)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
GT(s(x), s(y)) → GT(x, y)
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
IF(true, x, y) → MINUS(x, y)
MINUS(s(x), y) → IF(gt(s(x), y), x, y)
minus(s(x), y) → if(gt(s(x), y), x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
gcd(x, y) → if1(ge(x, y), x, y)
if1(true, x, y) → if2(gt(y, 0), x, y)
if1(false, x, y) → if3(gt(x, 0), x, y)
if2(true, x, y) → gcd(minus(x, y), y)
if2(false, x, y) → x
if3(true, x, y) → gcd(x, minus(y, x))
if3(false, x, y) → y
gt(0, y) → false
gt(s(x), 0) → true
gt(s(x), s(y)) → gt(x, y)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
gcd(x0, x1)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
if3(true, x0, x1)
if3(false, x0, x1)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
IF(true, x, y) → MINUS(x, y)
MINUS(s(x), y) → IF(gt(s(x), y), x, y)
gt(s(x), 0) → true
gt(s(x), s(y)) → gt(x, y)
gt(0, y) → false
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
gcd(x0, x1)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
if3(true, x0, x1)
if3(false, x0, x1)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
gcd(x0, x1)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
if3(true, x0, x1)
if3(false, x0, x1)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
IF(true, x, y) → MINUS(x, y)
MINUS(s(x), y) → IF(gt(s(x), y), x, y)
gt(s(x), 0) → true
gt(s(x), s(y)) → gt(x, y)
gt(0, y) → false
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
From the DPs we obtained the following set of size-change graphs:
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
IF2(true, x, y) → GCD(minus(x, y), y)
GCD(x, y) → IF1(ge(x, y), x, y)
IF1(true, x, y) → IF2(gt(y, 0), x, y)
IF1(false, x, y) → IF3(gt(x, 0), x, y)
IF3(true, x, y) → GCD(x, minus(y, x))
minus(s(x), y) → if(gt(s(x), y), x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
gcd(x, y) → if1(ge(x, y), x, y)
if1(true, x, y) → if2(gt(y, 0), x, y)
if1(false, x, y) → if3(gt(x, 0), x, y)
if2(true, x, y) → gcd(minus(x, y), y)
if2(false, x, y) → x
if3(true, x, y) → gcd(x, minus(y, x))
if3(false, x, y) → y
gt(0, y) → false
gt(s(x), 0) → true
gt(s(x), s(y)) → gt(x, y)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
gcd(x0, x1)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
if3(true, x0, x1)
if3(false, x0, x1)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
IF2(true, x, y) → GCD(minus(x, y), y)
GCD(x, y) → IF1(ge(x, y), x, y)
IF1(true, x, y) → IF2(gt(y, 0), x, y)
IF1(false, x, y) → IF3(gt(x, 0), x, y)
IF3(true, x, y) → GCD(x, minus(y, x))
gt(0, y) → false
gt(s(x), 0) → true
minus(s(x), y) → if(gt(s(x), y), x, y)
gt(s(x), s(y)) → gt(x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
gcd(x0, x1)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
if3(true, x0, x1)
if3(false, x0, x1)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
gcd(x0, x1)
if1(true, x0, x1)
if1(false, x0, x1)
if2(true, x0, x1)
if2(false, x0, x1)
if3(true, x0, x1)
if3(false, x0, x1)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
IF2(true, x, y) → GCD(minus(x, y), y)
GCD(x, y) → IF1(ge(x, y), x, y)
IF1(true, x, y) → IF2(gt(y, 0), x, y)
IF1(false, x, y) → IF3(gt(x, 0), x, y)
IF3(true, x, y) → GCD(x, minus(y, x))
gt(0, y) → false
gt(s(x), 0) → true
minus(s(x), y) → if(gt(s(x), y), x, y)
gt(s(x), s(y)) → gt(x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
GCD(0, s(x0)) → IF1(false, 0, s(x0))
GCD(x0, 0) → IF1(true, x0, 0)
GCD(s(x0), s(x1)) → IF1(ge(x0, x1), s(x0), s(x1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
IF2(true, x, y) → GCD(minus(x, y), y)
IF1(true, x, y) → IF2(gt(y, 0), x, y)
IF1(false, x, y) → IF3(gt(x, 0), x, y)
IF3(true, x, y) → GCD(x, minus(y, x))
GCD(0, s(x0)) → IF1(false, 0, s(x0))
GCD(x0, 0) → IF1(true, x0, 0)
GCD(s(x0), s(x1)) → IF1(ge(x0, x1), s(x0), s(x1))
gt(0, y) → false
gt(s(x), 0) → true
minus(s(x), y) → if(gt(s(x), y), x, y)
gt(s(x), s(y)) → gt(x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
IF1(true, y0, s(x0)) → IF2(true, y0, s(x0))
IF1(true, y0, 0) → IF2(false, y0, 0)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
IF2(true, x, y) → GCD(minus(x, y), y)
IF1(false, x, y) → IF3(gt(x, 0), x, y)
IF3(true, x, y) → GCD(x, minus(y, x))
GCD(0, s(x0)) → IF1(false, 0, s(x0))
GCD(x0, 0) → IF1(true, x0, 0)
GCD(s(x0), s(x1)) → IF1(ge(x0, x1), s(x0), s(x1))
IF1(true, y0, s(x0)) → IF2(true, y0, s(x0))
IF1(true, y0, 0) → IF2(false, y0, 0)
gt(0, y) → false
gt(s(x), 0) → true
minus(s(x), y) → if(gt(s(x), y), x, y)
gt(s(x), s(y)) → gt(x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
GCD(0, s(x0)) → IF1(false, 0, s(x0))
IF1(false, x, y) → IF3(gt(x, 0), x, y)
IF3(true, x, y) → GCD(x, minus(y, x))
GCD(s(x0), s(x1)) → IF1(ge(x0, x1), s(x0), s(x1))
IF1(true, y0, s(x0)) → IF2(true, y0, s(x0))
IF2(true, x, y) → GCD(minus(x, y), y)
gt(0, y) → false
gt(s(x), 0) → true
minus(s(x), y) → if(gt(s(x), y), x, y)
gt(s(x), s(y)) → gt(x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
IF1(false, 0, y1) → IF3(false, 0, y1)
IF1(false, s(x0), y1) → IF3(true, s(x0), y1)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
GCD(0, s(x0)) → IF1(false, 0, s(x0))
IF3(true, x, y) → GCD(x, minus(y, x))
GCD(s(x0), s(x1)) → IF1(ge(x0, x1), s(x0), s(x1))
IF1(true, y0, s(x0)) → IF2(true, y0, s(x0))
IF2(true, x, y) → GCD(minus(x, y), y)
IF1(false, 0, y1) → IF3(false, 0, y1)
IF1(false, s(x0), y1) → IF3(true, s(x0), y1)
gt(0, y) → false
gt(s(x), 0) → true
minus(s(x), y) → if(gt(s(x), y), x, y)
gt(s(x), s(y)) → gt(x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
GCD(s(x0), s(x1)) → IF1(ge(x0, x1), s(x0), s(x1))
IF1(true, y0, s(x0)) → IF2(true, y0, s(x0))
IF2(true, x, y) → GCD(minus(x, y), y)
IF1(false, s(x0), y1) → IF3(true, s(x0), y1)
IF3(true, x, y) → GCD(x, minus(y, x))
gt(0, y) → false
gt(s(x), 0) → true
minus(s(x), y) → if(gt(s(x), y), x, y)
gt(s(x), s(y)) → gt(x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
IF2(true, s(x0), x1) → GCD(if(gt(s(x0), x1), x0, x1), x1)
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
GCD(s(x0), s(x1)) → IF1(ge(x0, x1), s(x0), s(x1))
IF1(true, y0, s(x0)) → IF2(true, y0, s(x0))
IF1(false, s(x0), y1) → IF3(true, s(x0), y1)
IF3(true, x, y) → GCD(x, minus(y, x))
IF2(true, s(x0), x1) → GCD(if(gt(s(x0), x1), x0, x1), x1)
gt(0, y) → false
gt(s(x), 0) → true
minus(s(x), y) → if(gt(s(x), y), x, y)
gt(s(x), s(y)) → gt(x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
IF3(true, x1, s(x0)) → GCD(x1, if(gt(s(x0), x1), x0, x1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Instantiation
GCD(s(x0), s(x1)) → IF1(ge(x0, x1), s(x0), s(x1))
IF1(true, y0, s(x0)) → IF2(true, y0, s(x0))
IF1(false, s(x0), y1) → IF3(true, s(x0), y1)
IF2(true, s(x0), x1) → GCD(if(gt(s(x0), x1), x0, x1), x1)
IF3(true, x1, s(x0)) → GCD(x1, if(gt(s(x0), x1), x0, x1))
gt(0, y) → false
gt(s(x), 0) → true
minus(s(x), y) → if(gt(s(x), y), x, y)
gt(s(x), s(y)) → gt(x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
IF1(true, s(z0), s(z1)) → IF2(true, s(z0), s(z1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
GCD(s(x0), s(x1)) → IF1(ge(x0, x1), s(x0), s(x1))
IF1(false, s(x0), y1) → IF3(true, s(x0), y1)
IF2(true, s(x0), x1) → GCD(if(gt(s(x0), x1), x0, x1), x1)
IF3(true, x1, s(x0)) → GCD(x1, if(gt(s(x0), x1), x0, x1))
IF1(true, s(z0), s(z1)) → IF2(true, s(z0), s(z1))
gt(0, y) → false
gt(s(x), 0) → true
minus(s(x), y) → if(gt(s(x), y), x, y)
gt(s(x), s(y)) → gt(x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
IF1(false, s(z0), s(z1)) → IF3(true, s(z0), s(z1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
GCD(s(x0), s(x1)) → IF1(ge(x0, x1), s(x0), s(x1))
IF2(true, s(x0), x1) → GCD(if(gt(s(x0), x1), x0, x1), x1)
IF3(true, x1, s(x0)) → GCD(x1, if(gt(s(x0), x1), x0, x1))
IF1(true, s(z0), s(z1)) → IF2(true, s(z0), s(z1))
IF1(false, s(z0), s(z1)) → IF3(true, s(z0), s(z1))
gt(0, y) → false
gt(s(x), 0) → true
minus(s(x), y) → if(gt(s(x), y), x, y)
gt(s(x), s(y)) → gt(x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
IF2(true, s(z0), s(z1)) → GCD(if(gt(s(z0), s(z1)), z0, s(z1)), s(z1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Rewriting
GCD(s(x0), s(x1)) → IF1(ge(x0, x1), s(x0), s(x1))
IF3(true, x1, s(x0)) → GCD(x1, if(gt(s(x0), x1), x0, x1))
IF1(true, s(z0), s(z1)) → IF2(true, s(z0), s(z1))
IF1(false, s(z0), s(z1)) → IF3(true, s(z0), s(z1))
IF2(true, s(z0), s(z1)) → GCD(if(gt(s(z0), s(z1)), z0, s(z1)), s(z1))
gt(0, y) → false
gt(s(x), 0) → true
minus(s(x), y) → if(gt(s(x), y), x, y)
gt(s(x), s(y)) → gt(x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
IF2(true, s(z0), s(z1)) → GCD(if(gt(z0, z1), z0, s(z1)), s(z1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Rewriting
↳ QDP
↳ Instantiation
GCD(s(x0), s(x1)) → IF1(ge(x0, x1), s(x0), s(x1))
IF3(true, x1, s(x0)) → GCD(x1, if(gt(s(x0), x1), x0, x1))
IF1(true, s(z0), s(z1)) → IF2(true, s(z0), s(z1))
IF1(false, s(z0), s(z1)) → IF3(true, s(z0), s(z1))
IF2(true, s(z0), s(z1)) → GCD(if(gt(z0, z1), z0, s(z1)), s(z1))
gt(0, y) → false
gt(s(x), 0) → true
minus(s(x), y) → if(gt(s(x), y), x, y)
gt(s(x), s(y)) → gt(x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
IF3(true, s(z0), s(z1)) → GCD(s(z0), if(gt(s(z1), s(z0)), z1, s(z0)))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Rewriting
↳ QDP
↳ Instantiation
↳ QDP
↳ Rewriting
GCD(s(x0), s(x1)) → IF1(ge(x0, x1), s(x0), s(x1))
IF1(true, s(z0), s(z1)) → IF2(true, s(z0), s(z1))
IF1(false, s(z0), s(z1)) → IF3(true, s(z0), s(z1))
IF2(true, s(z0), s(z1)) → GCD(if(gt(z0, z1), z0, s(z1)), s(z1))
IF3(true, s(z0), s(z1)) → GCD(s(z0), if(gt(s(z1), s(z0)), z1, s(z0)))
gt(0, y) → false
gt(s(x), 0) → true
minus(s(x), y) → if(gt(s(x), y), x, y)
gt(s(x), s(y)) → gt(x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
IF3(true, s(z0), s(z1)) → GCD(s(z0), if(gt(z1, z0), z1, s(z0)))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Rewriting
↳ QDP
↳ Instantiation
↳ QDP
↳ Rewriting
↳ QDP
↳ Induction-Processor
GCD(s(x0), s(x1)) → IF1(ge(x0, x1), s(x0), s(x1))
IF1(true, s(z0), s(z1)) → IF2(true, s(z0), s(z1))
IF1(false, s(z0), s(z1)) → IF3(true, s(z0), s(z1))
IF2(true, s(z0), s(z1)) → GCD(if(gt(z0, z1), z0, s(z1)), s(z1))
IF3(true, s(z0), s(z1)) → GCD(s(z0), if(gt(z1, z0), z1, s(z0)))
gt(0, y) → false
gt(s(x), 0) → true
minus(s(x), y) → if(gt(s(x), y), x, y)
gt(s(x), s(y)) → gt(x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
POL(0) = 0
POL(GCD(x1, x2)) = x1
POL(IF1(x1, x2, x3)) = x2
POL(IF2(x1, x2, x3)) = x2
POL(IF3(x1, x2, x3)) = x2
POL(false) = 1
POL(ge(x1, x2)) = 1 + x1
POL(gt(x1, x2)) = 1
POL(if(x1, x2, x3)) = x1 + x2
POL(minus(x1, x2)) = x1
POL(s(x1)) = 1 + x1
POL(true) = 1
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Rewriting
↳ QDP
↳ Instantiation
↳ QDP
↳ Rewriting
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ DependencyGraphProof
↳ QTRS
GCD(s(x0), s(x1)) → IF1(ge(x0, x1), s(x0), s(x1))
IF1(true, s(z0), s(z1)) → IF2(true, s(z0), s(z1))
IF1(false, s(z0), s(z1)) → IF3(true, s(z0), s(z1))
IF3(true, s(z0), s(z1)) → GCD(s(z0), if(gt(z1, z0), z1, s(z0)))
gt(0, y) → false
gt(s(x), 0) → true
minus(s(x), y) → if(gt(s(x), y), x, y)
gt(s(x), s(y)) → gt(x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Rewriting
↳ QDP
↳ Instantiation
↳ QDP
↳ Rewriting
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Induction-Processor
↳ QTRS
IF1(false, s(z0), s(z1)) → IF3(true, s(z0), s(z1))
IF3(true, s(z0), s(z1)) → GCD(s(z0), if(gt(z1, z0), z1, s(z0)))
GCD(s(x0), s(x1)) → IF1(ge(x0, x1), s(x0), s(x1))
gt(0, y) → false
gt(s(x), 0) → true
minus(s(x), y) → if(gt(s(x), y), x, y)
gt(s(x), s(y)) → gt(x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
POL(0) = 0
POL(GCD(x1, x2)) = x2
POL(IF1(x1, x2, x3)) = x3
POL(IF3(x1, x2, x3)) = x3
POL(false) = 0
POL(ge(x1, x2)) = x1
POL(gt(x1, x2)) = 0
POL(if(x1, x2, x3)) = 1 + x2
POL(minus(x1, x2)) = x1
POL(s(x1)) = 1 + x1
POL(true) = 0
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Rewriting
↳ QDP
↳ Instantiation
↳ QDP
↳ Rewriting
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ DependencyGraphProof
↳ QTRS
↳ QTRS
IF1(false, s(z0), s(z1)) → IF3(true, s(z0), s(z1))
GCD(s(x0), s(x1)) → IF1(ge(x0, x1), s(x0), s(x1))
gt(0, y) → false
gt(s(x), 0) → true
minus(s(x), y) → if(gt(s(x), y), x, y)
gt(s(x), s(y)) → gt(x, y)
if(true, x, y) → s(minus(x, y))
if(false, x, y) → 0
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
minus(s(x0), x1)
if(true, x0, x1)
if(false, x0, x1)
gt(0, x0)
gt(s(x0), 0)
gt(s(x0), s(x1))
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Rewriting
↳ QDP
↳ Instantiation
↳ QDP
↳ Rewriting
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ QTRSRRRProof
↳ QTRS
minus'(s(x14), y10) → if'(gt(s(x14), y10), x14, y10)
if'(true, x32, y24) → minus'(x32, y24)
if'(false, x41, y31) → true
minus'(0, x1) → false
gt(0, y') → false
gt(s(x5), 0) → true
minus(s(x14), y10) → if(gt(s(x14), y10), x14, y10)
gt(s(x23), s(y17)) → gt(x23, y17)
if(true, x32, y24) → s(minus(x32, y24))
if(false, x41, y31) → 0
ge(x50, 0) → true
ge(0, s(x59)) → false
ge(s(x68), s(y50)) → ge(x68, y50)
minus(0, x1) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a23](0, 0) → true
equal_sort[a23](0, s(x0)) → false
equal_sort[a23](s(x0), 0) → false
equal_sort[a23](s(x0), s(x1)) → equal_sort[a23](x0, x1)
equal_sort[a41](witness_sort[a41], witness_sort[a41]) → true
minus'(s(x14), y10) → if'(gt(s(x14), y10), x14, y10)
if'(true, x32, y24) → minus'(x32, y24)
if'(false, x41, y31) → true
minus'(0, x1) → false
gt(0, y') → false
gt(s(x5), 0) → true
minus(s(x14), y10) → if(gt(s(x14), y10), x14, y10)
gt(s(x23), s(y17)) → gt(x23, y17)
if(true, x32, y24) → s(minus(x32, y24))
if(false, x41, y31) → 0
ge(x50, 0) → true
ge(0, s(x59)) → false
ge(s(x68), s(y50)) → ge(x68, y50)
minus(0, x1) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a23](0, 0) → true
equal_sort[a23](0, s(x0)) → false
equal_sort[a23](s(x0), 0) → false
equal_sort[a23](s(x0), s(x1)) → equal_sort[a23](x0, x1)
equal_sort[a41](witness_sort[a41], witness_sort[a41]) → true
[true, false, 0, minus2, if3, ge2, not1, equalsort[a41]2] > s1 > [minus'2, if'3] > gt2
equalbool2 > gt2
and2 > gt2
or2 > gt2
isatrue1 > gt2
isafalse1 > gt2
equalsort[a23]2 > gt2
witnesssort[a41] > gt2
equalsort[a23]2: multiset
minus2: [2,1]
minus'2: [1,2]
true: multiset
or2: multiset
equalsort[a41]2: [1,2]
and2: multiset
gt2: multiset
0: multiset
equalbool2: multiset
if3: [3,2,1]
if'3: [2,3,1]
witnesssort[a41]: multiset
not1: multiset
isafalse1: [1]
false: multiset
s1: multiset
ge2: multiset
isatrue1: multiset
minus'(s(x14), y10) → if'(gt(s(x14), y10), x14, y10)
if'(true, x32, y24) → minus'(x32, y24)
if'(false, x41, y31) → true
minus'(0, x1) → false
gt(0, y') → false
gt(s(x5), 0) → true
minus(s(x14), y10) → if(gt(s(x14), y10), x14, y10)
gt(s(x23), s(y17)) → gt(x23, y17)
if(true, x32, y24) → s(minus(x32, y24))
if(false, x41, y31) → 0
ge(x50, 0) → true
ge(0, s(x59)) → false
ge(s(x68), s(y50)) → ge(x68, y50)
minus(0, x1) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a23](0, 0) → true
equal_sort[a23](0, s(x0)) → false
equal_sort[a23](s(x0), 0) → false
equal_sort[a23](s(x0), s(x1)) → equal_sort[a23](x0, x1)
equal_sort[a41](witness_sort[a41], witness_sort[a41]) → true
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Rewriting
↳ QDP
↳ Instantiation
↳ QDP
↳ Rewriting
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ QTRSRRRProof
↳ QTRS
↳ RisEmptyProof
↳ RisEmptyProof
↳ RisEmptyProof
↳ QTRS
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Rewriting
↳ QDP
↳ Instantiation
↳ QDP
↳ Rewriting
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ QTRSRRRProof
minus'(s(x14), y10) → if'(gt(s(x14), y10), x14, y10)
if'(true, x32, y24) → minus'(x32, y24)
if'(false, x41, y31) → true
minus'(0, x1) → false
gt(0, y') → false
gt(s(x5), 0) → true
minus(s(x14), y10) → if(gt(s(x14), y10), x14, y10)
gt(s(x23), s(y17)) → gt(x23, y17)
if(true, x32, y24) → s(minus(x32, y24))
if(false, x41, y31) → 0
ge(x50, 0) → true
ge(0, s(x59)) → false
ge(s(x68), s(y50)) → ge(x68, y50)
minus(0, x1) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a27](0, 0) → true
equal_sort[a27](0, s(x0)) → false
equal_sort[a27](s(x0), 0) → false
equal_sort[a27](s(x0), s(x1)) → equal_sort[a27](x0, x1)
equal_sort[a44](witness_sort[a44], witness_sort[a44]) → true
minus'(s(x14), y10) → if'(gt(s(x14), y10), x14, y10)
if'(true, x32, y24) → minus'(x32, y24)
if'(false, x41, y31) → true
minus'(0, x1) → false
gt(0, y') → false
gt(s(x5), 0) → true
minus(s(x14), y10) → if(gt(s(x14), y10), x14, y10)
gt(s(x23), s(y17)) → gt(x23, y17)
if(true, x32, y24) → s(minus(x32, y24))
if(false, x41, y31) → 0
ge(x50, 0) → true
ge(0, s(x59)) → false
ge(s(x68), s(y50)) → ge(x68, y50)
minus(0, x1) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a27](0, 0) → true
equal_sort[a27](0, s(x0)) → false
equal_sort[a27](s(x0), 0) → false
equal_sort[a27](s(x0), s(x1)) → equal_sort[a27](x0, x1)
equal_sort[a44](witness_sort[a44], witness_sort[a44]) → true
[minus'2, if'3] > s1 > [false, ge2, equalbool2] > [true, witnesssort[a44]] > gt2
[minus2, if3] > s1 > [false, ge2, equalbool2] > [true, witnesssort[a44]] > gt2
[minus2, if3] > 0 > [false, ge2, equalbool2] > [true, witnesssort[a44]] > gt2
and2 > [false, ge2, equalbool2] > [true, witnesssort[a44]] > gt2
or2 > [true, witnesssort[a44]] > gt2
not1 > [false, ge2, equalbool2] > [true, witnesssort[a44]] > gt2
isatrue1 > [false, ge2, equalbool2] > [true, witnesssort[a44]] > gt2
isafalse1 > [false, ge2, equalbool2] > [true, witnesssort[a44]] > gt2
equalsort[a27]2 > [false, ge2, equalbool2] > [true, witnesssort[a44]] > gt2
equalsort[a44]2 > [true, witnesssort[a44]] > gt2
minus2: [2,1]
minus'2: [2,1]
true: multiset
or2: multiset
and2: [2,1]
gt2: multiset
0: multiset
equalsort[a44]2: multiset
witnesssort[a44]: multiset
equalbool2: [2,1]
if3: [3,2,1]
if'3: [3,2,1]
equalsort[a27]2: multiset
not1: multiset
isafalse1: [1]
false: multiset
s1: multiset
ge2: [1,2]
isatrue1: multiset
minus'(s(x14), y10) → if'(gt(s(x14), y10), x14, y10)
if'(true, x32, y24) → minus'(x32, y24)
if'(false, x41, y31) → true
minus'(0, x1) → false
gt(0, y') → false
gt(s(x5), 0) → true
minus(s(x14), y10) → if(gt(s(x14), y10), x14, y10)
gt(s(x23), s(y17)) → gt(x23, y17)
if(true, x32, y24) → s(minus(x32, y24))
if(false, x41, y31) → 0
ge(x50, 0) → true
ge(0, s(x59)) → false
ge(s(x68), s(y50)) → ge(x68, y50)
minus(0, x1) → 0
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a27](0, 0) → true
equal_sort[a27](0, s(x0)) → false
equal_sort[a27](s(x0), 0) → false
equal_sort[a27](s(x0), s(x1)) → equal_sort[a27](x0, x1)
equal_sort[a44](witness_sort[a44], witness_sort[a44]) → true
↳ QTRS
↳ Overlay + Local Confluence
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ Narrowing
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Instantiation
↳ QDP
↳ Rewriting
↳ QDP
↳ Instantiation
↳ QDP
↳ Rewriting
↳ QDP
↳ Induction-Processor
↳ AND
↳ QDP
↳ QTRS
↳ QTRSRRRProof
↳ QTRS
↳ RisEmptyProof
↳ RisEmptyProof
↳ RisEmptyProof